\begin{tabbing}
$\mathbb{Z}${-}rng
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<\mathbb{Z}$\+
\\[0ex], $\lambda$$u$,$v$. ($u$ =$_{0}$ $v$)
\\[0ex], $\lambda$$u$,$v$. $u$ $\leq$z $v$
\\[0ex], $\lambda$$u$,$v$. $u$+$v$
\\[0ex], 0
\\[0ex], $\lambda$$u$.{-}$u$
\\[0ex], $\lambda$$u$,$v$. $u$ $\ast$ $v$
\\[0ex], 1
\\[0ex], $\lambda$$u$,$v$. if ($v$ =$_{0}$ 0) then inr $\cdot$  else inl ($u$ $\div$ $v$)  fi $>$
\-
\end{tabbing}